COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	  RICHARD  there's lots of bugs, but the idea should be clear.
C00007 ENDMK
C⊗;
;  RICHARD  there's lots of bugs, but the idea should be clear.
;   let me know what you think; i'll be back here sat morening about 5:00
;   call if you want;  : 'till 3:30 today 739-7700 x6304; after: 353-2227

(SETQ DIR @(DIR TAUT TAUT1 
SIMP SIMPNOT SIMPOR SIMPAND SIMPANDOR
SIMPIMP SIMPEQUIV   MKOR MKAND  MKOR1 MKAND1 PN
FIRSTVAR  FIRSTVAR1 FIRSTVAR2))


(DE TAUT (WFF) (TAUT1 (SIMP WFF)))

(DE TAUT1 (W)  
 (COND( (ISCONST W) W)
        (T (TAUT 
	     ((LAMBDA (X) (MKAND (SUBST T X W) (SUBST NIL X W))) (FIRSTVAR W))))))


(DE SIMP (W) 
  (COND ((OR (ISCONST W) (ISVAR W)) W)
        ((ISNOT W)   (SIMPNOT (SIMP W)))
        ((ISOR W)    (SIMPOR (SIMP (ARG1 W))(SIMP(ARG2 W))))
        ((ISAND W)   (SIMPAND (SIMP (ARG1 W))(SIMP(ARG2 W))))
        ((ISIMP W)   (SIMPIMP (SIMP (ARG1 W))(SIMP(ARG2 W))))
        ((ISEQUIV W) (SIMPEQUIV (SIMP (ARG1 W))(SIMP(ARG2 W)))) )
)


(DE SIMPNOT (W) (COND ((ISFALSE W) T) ((ISTRUE W) NIL) (T (MKNOT W))))
(DE SIMPOR  (W1 W2) (SIMPANDOR @OR W1 W2 W1 W2))
(DE SIMPAND (W1 W2) (SIMPANDOR @AND W1 W2 W2 W1))
(DE SIMPIMP (W1 W2) (SIMPOR (SIMPNOT W1) W2))
(DE SIMPEQUIV (W1 W2)
    (SIMPAND (SIMPIMP W1 W2)(SIMPIMP W2 W1)))


; NICE DUALITY  IN AND AND OR


(DE SIMPANDOR (OP W1 W2 V1 V2)
  (COND	((ISTRUE W1) V1) 
	((ISTRUE W2) V2)
	((ISFALSE W1) V2)
	((ISFALSE W2) V1)
	(T (MKOP OP W1 W2))))


(DE MKOR (V L)(MKOR1 V (REST L) (MKAND W (REVERSE (FIRST L)))))

(DE MKOR1 (V L1 L2)(COND((NULL L1 ) L2)
	(T(MKOR1 V 
		(REST L1)
		(MKOP @OR  
		      (MKAND  V (REVERSE (FIRST L1))) 
		       L2)))))

))))))

(DE MKAND (V L)(COND ((ZEROP (FIRST L)) NIL)
			(T (MKAND1 (REST V)
					(REST(REST L))
					(COND ((ZEROP L)(MK_NOT (FIRST L)))
						(T (FIRST V)))))))

)))))
(DE MKAND1 (V L1 L2)(COND ((NULL L1) L2)
			(T (MKAND1	(REST V)
					(REST L1)
					(MKOP @AND
						(COND ((ZEROP L1)(MK_NOT (FIRST V)))
							(T (FIRST V)))))))
						L2)))))

)))))

(DE FIRSTVAR (W) (FIRSTVAR1 W NIL))

(DE FIRSTVAR1 (W VAR) (COND ((NOT (NULL VAR)) VAR)
				((ISCONST W) NIL)
				((ISVAR W) W)
				((UNARY W) (FIRSTVAR1 (BODY W) ()))
				(T (FIRSTVAR1 (LHS W)
					       ((LAMBDA (X) (COND (X X)
								(T(FIRSTVAR1 (RHS W)
									()))))
							(RHS W))))))
)))))

;alternative firstvar

(DE FIRSTVAR2 (W) (COND ((ISVAR W) W)
			((UNARY W) (FIRSTVAR (BODY W) ))
			((FIRSTVAR (LHS W))
			(T (FIRSTVAR (RHS W))))

; abstract pn

(DE PN (WFF Z)
  (COND ((ATOM WFF) (COND ( (ISOR Z) (MKNOT WFF) )
	   		    (T WFF)))
        ((ISNOT WFF) (PN (BODY WFF) (FLIP Z)))
		(ISEQUIV WFF) (MKOP Z

				    (MKOP (FLIP Z)

;  ETC, ETC
))))))